package verifier.property;

import org.jgrapht.Graph;
import org.jgrapht.graph.DefaultDirectedGraph;
import org.jgrapht.graph.DefaultEdge;

class Automata1 implements Cloneable {
    private StateNode start;
    private StateNode currentStateNode;
    private Graph<StateNode, AutomataEdge> graph;
    private int stateIdx = 0;
    public String source;

    public Automata1() {
        this.graph = new DefaultDirectedGraph<>(AutomataEdge.class);
        this.start = createStateNode();
        this.graph.addVertex(start);
    }

    public Automata1(String regex) {
        this.graph = new DefaultDirectedGraph<>(AutomataEdge.class);
        this.start = createStateNode();
        this.graph.addVertex(start);

        String[] elements = regex.split(",");
        this.source = elements[0];

        StateNode lastStateNode = this.start;
        for (String element : elements) {
            if (element.equals(".*")) {
                this.graph.addEdge(lastStateNode, lastStateNode, new AutomataEdge("."));
            } else {
                StateNode next = createStateNode();
                this.graph.addVertex(next);
                this.graph.addEdge(lastStateNode, next, new AutomataEdge(element));
                lastStateNode = next;
            }
        }
        lastStateNode.setEnd();
        init();
    }

//    public void product(Automata automata) {
//        for (StateNode stateNode : this.graph.vertexSet()) {
//            for (StateNode stateNode1 : automata.vertexSet()) {
//                StateNode stateNode2 = new StateNode()
//            }
//        }
//    }

    public void addStateNode(String label) {
        this.graph.addVertex(new StateNode(label));
    }

    public java.util.Set<StateNode> vertexSet() {
        return this.graph.vertexSet();
    }

    private StateNode createStateNode() {
        return new StateNode(stateIdx++);
    }

    public void init() {
        this.currentStateNode = this.start;
    }

    public boolean isFinal() {
        return this.currentStateNode.isEnd;
    }

    // true: acceptable symbol, false: otherwise
    public boolean transfer(String symbol) {
        boolean hasAny = false;
        for (AutomataEdge e : this.graph.outgoingEdgesOf(this.currentStateNode)) {
            if (e.getLabel().equals(".")) {
                hasAny = true;
            }
            if (e.getLabel().equals(symbol)) {
                currentStateNode = graph.getEdgeTarget(e);
                return true;
            }
        }

        // no action can match, and do not exist .*
        if (!hasAny) {
            currentStateNode = null;
            return false;
        }
        return true;
    }

    public Object clone()throws CloneNotSupportedException{
        return super.clone();
    }

    private class AutomataEdge extends DefaultEdge {
        private String label;

        public AutomataEdge(String label) {
            this.label = label;
        }

        public String getLabel() {
            return label;
        }
    }

    public class StateNode {
        private String label;
        protected Boolean isStart = false;
        protected Boolean isEnd = false;

        public StateNode(int label) {
            this.label = String.valueOf(label);
        }

        public StateNode(String label) {
            this.label = label;
        }

        @Override
        public String toString() {
            return label;
        }

        public void setEnd() {
            this.isEnd = true;
        }

        public boolean isEnd() {
            return this.isEnd;
        }
    }

    public static void main(String[] args) {
//        Automata a = new Automata("a,.*,b,c");
//        System.out.println(a.transfer("a"));
//        System.out.println(a.transfer("i"));
//        System.out.println(a.transfer("d"));
//        System.out.println(a.transfer("b"));
//        System.out.println(a.transfer("cj"));
    }
}